.if xcribl then hauwide ← 80 else hauwide ← 70
.page frame 59 high (hauwide) wide
.text area text lines 5 to 56
.title area heading line 1
.title area footing line 59
.place text
.turn on "%#{α↓_&[]"
.turn on "↑" for "\"    << need backslash for ECL code >>
.turn on "`" for "↑"    << need something for superscripts >>
.turn off "-"
.font 1 "25fr1"           << text >>
.font 2 "25fri1"         << italics >>
.font 3 "25fg"          << ECL code >>
.font 4 "gls;foo"     << weird characters >>
.font 5 "36vbee"         << headings >>
.headfont ← 5
.tabbreak
.at null ⊂ if not filling then skip 1 ⊃
.double space
.indent 8,0,0

.count ftnote inline printing "<1>"
.at ",," cruft """" ⊂  next ftnote; ! ;
.   send foot ⊂
.      select 1
.      preface 1
.      single space
.      indent 0,0
{!}  cruft
.      break ⊃ ⊃
.footsep ← "---------------------------------------------------"

.count chaptercount
.macro chapter(tag, title) ⊂
.   if lines < (5 * spread) then next page
.   tag: next chaptercount
.   skip (spread+2)
.   once nofill indent 0
.   select headfont
{!}.   title
.   skip 1 ⊃

.count sectioncount in chaptercount printing "!.1"
.macro section(tag, title) ⊂
.   if lines < (5 * spread) then next page
.   tag: next sectioncount
.   skip (spread+2)
.   once nofill indent 0
.   select headfont
{!}.   title
.   skip 1 ⊃

.count subsectioncount in sectioncount printing "!.1"
.macro subsection(tag, title) ⊂
.   if lines < (5 * spread) then next page
.   tag: next subsectioncount
.   skip (spread+2)
.   once nofill indent 0
.   select headfont
{!}.   title
.   skip 1 ⊃

.count subsubseccount in subsubsectioncount printing "!.1"
.macro subsubsec(tag, title) ⊂
.   if lines < (5 * spread) then next page
.   tag: next subsubseccount
.   skip (spread+2)
.   once nofill indent 0
.   select headfont
{!}.   title
.   skip 1 ⊃

.macro smallhead(title) ⊂
.   if lines < (5 * spread) then next page
.   skip (spread+1)
.   once nofill indent 0
.   select 1
↓_title_↓
.   skip 1 ⊃

.macro beginecl ⊂
.   begin group
.   nofill
.   indent 0,0
.   narrow 4,0
.   tabs 5,9,13,17,21,25,29,33,37,41
.   select 3
.   skip spread ⊃

.macro endecl ⊂
.   skip 1
.   end 
.   continue ⊃

.macro osem ⊂
.   if xcribl then start }%4O%*{ end
.      else start turn on "∂"
.             }O∂-1O∂-1O∂-1O∂-1O∂-1O∂-1O{
.             turn off "∂" end ⊃

.macro psem ⊂
.   if xcribl then start }%4P%*{ end
.      else start turn on "∂"
.             }P∂-1P∂-1P∂-1P∂-1P∂-1P∂-1P{
.             turn off "∂" end ⊃

.macro rsem ⊂
.   if xcribl then start }%4R%*{ end
.      else start turn on "∂"
.             }R∂-1R∂-1R∂-1R∂-1R∂-1R∂-1R{
.             turn off "∂" end ⊃

.macro ssem ⊂
.   if xcribl then start }%4S%*{ end
.      else start turn on "∂"
.             }S∂-1S∂-1S∂-1S∂-1S∂-1S∂-1S{
.             turn off "∂" end ⊃

.macro vsem ⊂
.   if xcribl then start }%4V%*{ end
.      else start turn on "∂"
.             }V∂-1V∂-1V∂-1V∂-1V∂-1V∂-1V{
.             turn off "∂" end ⊃

.macro numsem ⊂
.   if xcribl then start }%4α#%*{ end
.      else start turn on "∂"
.             }α#∂-1α#∂-1α#∂-1α#∂-1α#∂-1α#∂-1α#{
.             turn off "∂" end ⊃

.macro dolsem ⊂
.   if xcribl then start }%4α$%*{ end
.      else start turn on "∂"
.             }α$∂-1α$∂-1α$∂-1α$∂-1α$∂-1α$∂-1α${
.             turn off "∂" end ⊃

.macro mu ⊂
.   if xcribl then start }%4∨%*{ end
.      else start turn on "∂"
.             }mu∂-2mu∂-2mu∂-2mu∂-2mu∂-2mu∂-2mu{
.             turn off "∂" end ⊃

.at "??" x "," j "," k "," t ";" ⊂ }↓[j]x↓[k]&`[t]{ ⊃

.at "P'(" sem ")" ⊂ psem(); }/(sem)/{ ⊃

.at "V'(" sem ")" ⊂ vsem(); }/(sem)/{ ⊃

.at "$" wds "$" ⊂
.   if xcribl then start }%2{}wds%*{ end
.             else start }↓_wds_↓{ end ⊃

.at "/" wds "/" ⊂
.   if xcribl then start }%3{}wds%*{ end
.             else start }↓_wds_↓{ end ⊃

.at "@" tag "@" ⊂
.   [2] tag ⊃

.at "∞" ⊂ }%4|%*↑{ ⊃

.at "→→" ⊂ }%4α→%*{ ⊃

.at "↔↔" ⊂ }%4α↔%*{ ⊃

.at "<=" ⊂
.   if xcribl then }%4←%*{
.      else start }<-{ end ⊃

.section semexplain,What Are Semaphores?

	Before considering the problem of generating
semaphore code, we would do well first to understand
thoroughly what we mean by a "semaphore".
In particular, there is a subtlety in the {psem}
operation on semaphores which must be understood
quite thoroughly, for the proof of a later theorem
[] will depend critically on this subtlety.
	Dijkstra [] defines semaphores and their
behavior as follows:
.begin narrow 4,8
.indent 0,8
.skip 1
	The semaphores are essentially non-negative inetegers.
	$Definition.$  The {vsem}-operation is an operation
with one argument, which must be the identification of
a semaphore.  (If "S1" and "S2" denote semaphores we can
write "{vsem}(S1)" and "{vsem}(S2)".)  Its function is to
increase the value of its argument semaphore by 1; this increase
is to be regarded as an indivisible operation.
	$Definition.$  The {psem}-operation is an operation
with one argument, which must be the identification of
a semaphore.  (If "S1" and "S2" denote semaphores we can
write "{psem}(S1)" and "{psem}(S2)".)  Its function is to
decrease the value of its argument semaphore by 1 as soon as
the resulting value would be non-negative.  The completion
of the {psem}-operation -- i.e. the decision that this is
the appropriate moment to effectuate the decrease and the
subsequent decrease itself -- is to be regarded as an
indivisible operation.
.skip 1
.end
.continue
Now these definitions seem to be perfectly straightforward;
indeed it is their apparent simplicity which makes semaphores
so widely used in solutions of synchronization problems.
	There is, however, one very subtle phrase in
the definition of the {psem}-operation: "as soon as".
What does this mean?  The phrase "as soon as"
implies a comparison of the times of two events,
namely the incrementation of the semaphore from zero
(presumably by a {vsem}-operation) and
the completion of the {psem}-operation.
We might try to formalize this notion by saying,
"In the total ordering of all the discrete events in our system,
there is no event x such that x occurs after the {vsem}-operation
but before the {psem}-operation which was pending."
At first sight this seems to be exactly what we mean;
but the notion collapses when we realize that in a system
with multiple processes, there can be no total ordering on
events, but only a partial ordering; indeed, our very intent
in using semaphores is to enforce a particular partial ordering.
	Another question we might ask is:
what state is the process in when it attempts to perform a
{psem}-operation but cannot because the semaphore's value is zero?
The usual answer is: it is in a waiting state.  But this in itself
is quite vague;  indeed, most of the literature on multiple
processing is vague on this point.  For suppose that a process
in the course of its execution attempts to perform a {psem}-operation.
Now it must make a decision as to whether a decrementation
would leave the semaphore non-negative.  Our definition above
tells us what occurs if the result of the decision is "yes":
the semaphore is decremented.  But what if the result of
the decision is "no"?  The definition gives no clue as to what
happens.
	In order to decide how best to resolve these ambiguities,
let us consider how we might implement semaphores on a "typical"
contemporary computer system.  First let us consider, say,
two computers with a common memory on a common bus
(think, for example, of two PDP-11's).
We will assume that the computers have two instructions defined
as follows:
.beginecl
VSEM <loc>		(1)  Seize the memory bus.
		(2)  Fetch the word at location <loc>.
		(3)  Add 1 to this word.
		(4)  Store the word back into location <loc>.
		(5)  Release the memory bus.

PSEM <loc>		(1)  Seize the memory bus.
		(2)  Fetch the word at location <loc>.
		(3)  If not strictly positive, go to step (7).
		(4)  Subtract 1 from the word.
		(5)  Store the word back into location <loc>.
		(6)  Increment the program counter (to cause a skip).
		(7)  Release the memory bus.
.endecl
Designing such instructions into a computer like the PDP-11
is certainly possible
,,Indeed, the PDP-11 /INC/ instruction
and the PDP-10 /AOS/ instruction are
like the /VSEM/ instruction
we have defined.  Many computers have a $decrement and
skip if positive$ instruction (for example, the PDP-10's
/SOSG/ instruction), but these are usually implemented as
$decrement then skip if positive$ and therefore cannot be
used for the {psem}-operation.".
Note that the above "synchronization"
instructions are defined in terms of other synchronization
primitives, namely "seize the memory bus" and
"release the memory bus".  We will leave these primitives
undefined, just as Dijkstra left the terms "as soon as"
and "indivisible" undefined.
	We can then code the {psem} and {vsem} operations
as follows (in a mythical assembly language):
.beginecl
S1:	0		;$a semaphore, initially zero$

	VSEM S1		;$this is the encoding of$ {vsem}(S1)

LOOP:	PSEM S1		;$this is the encoding of$ {psem}(S1)
	JUMP LOOP
.endecl
That is, if the result of the decision is "no", then
we loop back and try again.  When, eventually, location
/S1/ becomes strictly positive, then the /PSEM/
instruction will decrement it and skip.
Because the processor attempting
to perform the {psem}-operation is busily looping until the
semaphore becomes positive, this is known as a "busy-wait"
implementation.
	One objection to the busy-wait implementation
is that the waiting processor continues to seize and release
the memory bus even though it is not accomplishing useful work;
this may have the effect of slowing down the other processor
unnecessarily because of bus contention.  Perhaps we would like
to consider an alternative implementation in which a waiting
processor takes no unnecessary bus cycles.  But if the waiting
processor takes no bus cycles, how can it know when the
semaphore becomes positive?  Well, the semaphore can become
positive only as the result of a {vsem}-operation.
Suppose then that the /VSEM/
instruction were modified to signal any waiting processors.
We could then define our instructions as follows:
.beginecl
VSEM <loc>		(1)  Seize the memory bus.
		(2)  Fetch the word at location <loc>.
		(3)  Add 1 to this word.
		(4)  Store the word back into location <loc>.
		(5)  Send a signal to all other processors.
		(5)  Release the memory bus.

PSEM <loc>		(1)  Seize the memory bus.
		(2)  Fetch the word at location <loc>.
		(3)  If strictly positive, go to step (6).
		(4)  Release the memory bus.
		(5)  Wait for the signal, then go to step (1).
		(6)  Subtract 1 from the word.
		(7)  Store the word back into location <loc>.
		(8)  Increment the program counter (to cause a skip).
		(9)  Release the memory bus.
.endecl
This alleviates the bus contention problem; but notice that in
order to do so we had to introduce some extra machinery,
namely an interprocessor signaling mechanism.
	Furthermore, the above solution is not quite optimal,
in that the signal is sent out when one processor performs
{vsem}/(S1)/ even if the other was trying to do {psem}/(S2)/.
Thus the waiting processor may be signalled only to have to wait
again.  This can be fixed up at the price of more machinery;
e.g. the signal could contain the address of the semaphore.
	Let us now consider another implementation environment,
a time-sharing system, where we wish to implement {psem} and
{vsem} as monitor callsα/supervisor callsα/system callsα/UUOs
(choose one).  For definiteness, let us define two UUOs for
a PDP-10 timesharing monitor called /.VSEM/ and /.PSEM/.
Here is an excerpt from the mythical manual for this
timesharing system:
.beginecl
 .VSEM <addr>	Increments the contents of location <addr>.
			Returns to calling location + 1.

 .PSEM <addr>	If the contents of location <addr> are positive,
		then the contents are decremented, and .PSEM returns
		to the calling location + 1.  If the contents are zero
		or negative, then the executing job is put to sleep
		until such time as the contents become positive (see the
		.SLEEP UUO).

	.VSEM and .PSEM are most useful when used on locations in
	a block of core shared by two or more jobs; they can then be
	used to synchronize the actions of the jobs.  See the .CBLK
	UUO for information on sharing core blocks.
.endecl
This is certainly typical of what one might see in a timesharing
handbook, and would suffice for most practical purposes.
For us, however, the phrase "until such time as" is just
ambiguous as the phrase "as soon as" in Dijkstra's definition.
Let us consider the internal implementation of /.VSEM/ and
/.PSEM/.
	Suppose that our monitor system maintains a series
of queues in which jobs are kept.  In particular, there are
two queues called the "run queue" and the "semaphore queue".
Jobs are scheduled at every tick of a real-time clock by
putting the currently running job at the end of the run queue
and taking a new job (perhaps the same one, if the run queue
was empty) from the front of the run queue; this new job is
then run until the next clock tick.  This is a standard
round-robin scheduler.
	Now there are several strategies one could take
in implementing /.PSEM/ and /.VSEM/, just as there were
several strategies in our dual-processor example.
Let us consider some of them.

.smallhead Semaphore Queuing

	When the currently running job performs a /.PSEM/,
the monitor checks the location addressed.  If it is positive,
the monitor decrements it, sets the job's program counter
to the location after the /.PSEM/, and continues running
the job.  Otherwise it sets the job's program counter to
the location after the /.PSEM/, and puts the job on the semaphore
queue, along with the information as to the location of the
semaphore.  The monitor then schedules a new job from the front
of the run queue.
	When the currently running job executes a /.VSEM/,
the monitor increments the addressed location, and sets
the job's program counter to the location after the /.VSEM/.
The monitor then scans down the semaphore queue, processing
each job on that queue in order.  For each job, if the
semaphore location that job was waiting for has become positive,
then the location is decremented and the job is spliced
out of the semaphore queue and put at the end of the run queue.
Note that if several jobs were waiting on the same semaphore,
the ones nearest the front of the semaphore queue (i.e. those which
have been waiting longest) are given priority.

.smallhead Semaphore Stacking

	Suppose that the monitor uses the semaphore queueing
scheme, but instead of maintaining a semaphore queue,
the monitor maintains a semaphore stack; i.e. it uses
a LIFO instead of FIFO discipline on the semaphore queue.
This scheme is certainly as valid as the straight queuing
scheme as far as Dijkstra's definition goes, but in practice
it could materially affect the performance of synchronized
processes, particularly if they depended in some way
on the ordering.

.smallhead Semaphore Bagging

	Suppose that the monitor uses the semaphore queueing
scheme, but instead of maintaining a semaphore queue,
the monitor maintains a semaphore "bag", i.e. an $unordered$
set of waiting jobs ,,Equivalently, let a queue be used,
but let the monitor not take particular care to maintain
the ordering of the queue, e.g. it arbitrarily re-orders
the queue when scanning it during a /.VSEM/.".
This is also just as valid a scheme as straight queuing.

.smallhead Busy Waiting

	In this implementation the semaphore queue is
not needed at all.
	When the currently running job performs a /.VSEM/,
the monitor merely increments the addressed location,
sets the job's program counter to the location after the
/.VSEM/, and continues running the job.
	When the currently running job performs a /.PSEM/,
the monitor checks the location addressed.  If it is positive,
the monitor decrements it, sets the job's program counter
to the location after the /.PSEM/, and continues running
the job.  Otherwise it sets the job's program counter to
the location of the /.PSEM/
,,Compare this to the /JUMP LOOP/ instruction in the
dual-processor implementation.",
puts the job at the end of the run queue, and schedules a new
job from the front of the run queue.
	The busy wait approach is actually rather reasonable
in a time-sharing situation if the overhead of switching jobs
and interpreting a /.PSEM/ is not too high.  If a job
is still blocked on a /.PSEM/, it will be scheduled, re-execute
the /.PSEM/, and then immediately be put back on the run queue.
	Note now, however, an interesting difference between
busy waiting and the various queuing methods.  Suppose we have
three jobs called /A/, /B/, and /C/.  Let their text be
as follows:
.beginecl
;;; $Semaphore$ S1 $is in a common block of core$.

;;; $process$ A
AGO:	.PSEM S1

;;; $process$ B
BGO:	.VSEM S1

;;; $process$ C
CGO:	.PSEM S1
.endecl
Let all the jobs be started up (put on the run queue)
with process /A/'s program counter at /AGO/, /B/'s at
/BGO/, and /C/'s at /CGO/.
	Suppose that we are using any
of the above queuing disciplines.
Process /A/ is scheduled, and it executes the /.PSEM/.
It is put on the semaphore queue, and another process is
scheduled.  Suppose this other process is /B/.
Then let /B/ execute the /.VSEM/; this will cause
process /A/ to be put back on the run queue.
Process /C/, no matter when subsequently scheduled,
will not ever complete its /.PSEM/, because it will
execute the /.PSEM/ $after$ /B/'s /.VSEM/.
	Now suppose that we are using the busy-wait
implementation.  Let process /A/ be scheduled as before,
execute the /.PSEM/, and be put at the end of the run
queue.  Then let process /B/ be scheduled and execute
the /.VSEM/.  After this let a clock tick occur and
let process /C/ be scheduled.  It will succeed in
completing the /.PSEM/ even though /A/ was already waiting,
and even though /C/'s /.PSEM/ was executed $after$
/B/'s /.VSEM/; process /A/ will hang forever.  On the other hand
if a clock tick occurred just before /C/'s /.PSEM/,
then process /A/ could re-execute its /.PSEM/, and
process /C/ would be permanently blocked.
Thus, depending on the capriciousness of the clock
(and of the scheduling discipline),
either /.PSEM/ could succeed even though one,
and only one, was
"actually waiting" when the /.VSEM/ occurred.
	Here, then, we see clearly the problem
in the phrase "as soon as".  In the busy-wait case,
process /A/ certainly does not perform its
/.PSEM/ "as soon as" possible, since in fact /C/ may get
in first; on the other hand, process /A/ certainly
gets in "as soon as" it can, if at all, in that it
devotes all of its share of the run time to trying to
push the /.PSEM/ to completion.  Thus, process /A/
completes the /.PSEM/ as soon as possible, but the system
as a whole may not.
	This is reasonable if we think of the case where the
processes run in the order /A/, /C/, /B/.
Suppose that process /A/ executes its /.PSEM/;
then process /C/ is scheduled and executes its /.PSEM/;
and finally process /B/ is scheduled and executes its
/.VSEM/.  Now clearly one or the other of
processes /A/ and /C/ may proceed, $but not both$.
In some sense, one feels intuitively, the one which does not
proceed has not performed its /.PSEM/ "as soon as"
possible;  furthermore Dijkstra's definition gives no clue
as to how the choice of which process to proceed should
be made.
	One could argue that it should be indeterministic,
since the rules don't specify the choice.  This makes sense
if we return to our idea of "as soon as" having meaning only
in a total time ordering.  In a multiple process system
only the events of a single process are totally ordered,
and so all we can say is that a {psem}-operation
completes as soon as $its executing process$
is able to do so.  How the conflict between processes
competing for completion of a {psem}-operation
is resolved is, as we have seen, a characteristic of
the particular implementation.
	As a final note, let us reconsider the question
of the state of a process which is trying to complete a /.PSEM/.
In particular, consider the value of a waiting job's
program counter.  Under the busy-waiting scheme,
the job's program counter is, when the job is not running,
seen to be before the /.PSEM/.  Under the queuing schemes,
however, the program counter cannot be before the /.PSEM/,
because the /.PSEM/ has had an effect, namely to put
the job on a different queue;  on the other hand, it cannot
truly be after the /.PSEM/ because that would imply that
the /.PSEM/ had completed and that the process should
continue.  Indeed, it appears that in this case the /.PSEM/
is not as indivisible as we would like to think;  the program
counter must be in limbo, halfway between
,,A real timesharing monitor (e.g. the ITS system at M.I.T.)
often resolves this problem by $undoing$ the effects of
a UUO before allowing another job to examine the waiting job.
In this case, if another job asked to examine the waiting job's
program counter, the monitor might first reset the waiting job's
program counter to point to the /.PSEM/ and take the job back
off the semaphore queue.  Of course, this involves
synchronizing mechanisms in the monitor other than /.PSEM/
and /.VSEM/; let us regard this as a piece of debugging
magic irrelevant to our main problem.".
We may think of /.PSEM/ internally being in two parts:
a "request" portion and a "success" portion.

.section semformal,A Formal Model of Semaphore Operations


	At this point it will be useful to
clarify formally the distinction between
queuing semaphores and busy-waiting semaphores.
In order to do this we have to formalize the notion
that a {psem} operation actually consists of two
parts, even though it is in theory "indivisible".
We shall divide the {psem} operation into two operations
{rsem} and {ssem} (meaning "request" and "succeed"),
and impose certain constraints on their use so that
the {psem} operation will be correctly modeled.

.smallhead Notation

	Let ??X,$j$,$k$,$t$; denote a semaphore event,
namely the operation X by process $j$ on semaphore $k$
at time $t$.  The operation X may be {vsem}, {rsem},
or {ssem}.  The time $t$ is a positive integer.
With respect to any given process or any given semaphore
there may or may not be an event at a given time $t$;
the concept of "time" is used only to order the events
of a process or on a semaphore.  It is possible
that there may be several events at the same time.
When we speak of the system "as of time $n$" we
mean just after the events, if any,
at time $n$ have taken place.
By "before time $n$" we mean just before the events
of time $n$, if any, have occurred.
We shall sometimes speak of "time 0"; as of this time
no events have occurred.
	We will find it convenient to consider sets
of events.  By
%3α{??{vsem},$j$,$k$,;α}%1, for example,
we mean %3α{??{vsem},$j$,$k$,$t$; ∀$t$α}%1, that is,
the set of all {vsem} operation executed at any time
by process $j$ on semaphore $k$.
Similarly, by %3α{??{rsem},,$k$,;α}%1 we mean
%3α{??{rsem},$j$,$k$,$t$; ∀$j$ ∀$t$α}%1.
	We will use the letter {osem} to stand for
any of {vsem}, {rsem}, {ssem} in this context:
thus %3α{??{osem},,,$t$;α}%1 means
%3α{??X,$j$,$k$,$t$; ∀Xεα{{vsem}, {rsem}, {ssem}α} ∀$j$ ∀$k$α}%1.
	All such sets do not necessarily contain all
possible elements; the universe of events is constrained
by the nature of the particular processes under
consideration, and will also be constrained by
a number of rules of elaboration which we will set forth
below.
	Let %3{mu}$t$[predicate]%1 have the usual
interpretation; namely, its value is the smallest value
of $t$ such that %3predicate%1 is true.
	By {numsem}S we will mean the number of elements
in the set S.  For example,
%3{numsem}α{{vsem}, {rsem}, {ssem}α} = 3%1.
	By %3??{numsem},,,$t$;S%1 we will mean
%3{numsem}(S ∩ α{??{osem},,,$t'$; | $t'$ ≤ $t$α})%1,
that is, those elements of %3S%1 which occurred at or
before time $t$.
	By %3($j$)$t$%1 we shall mean
%3{mu}$t'$($t'$ %4>%* t ∧ {numsem}α{??{osem},$j$,,$t$;α} %4>%* 0)%1,
that is, the smallest $t'$ greater than $t$ such that
there is an event involving process $j$ at time $t'$.
	Similarly, by %3$t$($k$)%1 we shall mean
%3{mu}$t'$($t'$ %4>%* t ∧ {numsem}α{??{osem},,$k$,$t$;α} %4>%* 0)%1,
that is, the smallest $t'$ greater than t such that
there is an event involving semaphore $k$ at time $t'$.
	Let %3N($k$)%1 be the "initial value" of semaphore $k$;
this is a non-negative integer.

.smallhead Basic Rules of Elaboration

.smallhead Rule 1.  Process Exclusivity

.beginecl
∀$j$ ∀$t$ {numsem}α{??{osem},$j$,,$t$;α} %4≤%* 1
.endecl
	That is, no process is involved in more than one
event at a time.  (At any given time it may be involved in one
event or no event.)

.smallhead Rule 2.  Semaphore Exclusivity

.beginecl
∀$k$ ∀$t$ {numsem}α{??{osem},,$k$,$t$;α} %4≤%* 1
.endecl
	That is, no semaphore is involved in more than one
event at a time.  (At any given time it may be involved in one
event or no event.)

.smallhead Rule 3.  Immediate Success

.beginecl
∀$t$ ∀$j$ ∀$k$ ??{rsem},$j$,$k$,$t$; ε α{??{osem},,,$t$;α} ∧ N($k$) + ??{numsem},,,$t$;α{??{vsem},,$k$,;α} %4>%* ??{numsem},,,$t$;α{??{ssem},,$k$,;α} →→ ??{ssem},$j$,$k$,$t$($k$); ε α{??{osem},,,$t$($k$);α}
.endecl
	That is, if a process performs an {rsem} operation
on a semaphore and that semaphore is not blocked (initial
value plus previous {vsem}'s exceed previous {ssem}'s)
then the next operation on that semaphore must be an
{ssem} involving the same process.  This means that
a process does not wait when it does a {psem} if
the semaphore is not blocked.

.smallhead(Rule 4.  Indivisibility of {psem} with Respect to the Executing Process)

.beginecl
∀$t$ ∀$j$ ∀$k$ ??{rsem},$j$,$k$,$t$; ε α{??{osem},,,$t$;α} →→ ??{ssem},$j$,$k$,$t$; ε α{??{osem},,,($j$)$t$;α}

∀$t$ ∀$j$ ∀$k$ ??{ssem},$j$,$k$,$t$; ε α{??{osem},,,$t$;α} →→  ??{numsem},,,$t-1$;α{??{rsem},$j$,$k$,;α} = ??{numsem},,,$t-1$;α{??{ssem},$j$,$k$,;α} + 1
.endecl
	That is, the only operation a process can possibly
perform next after an {rsem} on a given semaphore is
an {ssem} on the same semaphore.  Furthermore, an {ssem}
on a given semaphore must be preceded by an {rsem} by the
same process on the same semaphore.  This preserves our
notion that {rsem} and {ssem} are really two components
of an "indivisible" operation {psem}.

.smallhead(Rule 5.  Blocking Condition for {psem})

.beginecl
∀$t$ ∀$j$ ∀$k$ ??{ssem},$j$,$k$,$t$; ε α{??{osem},,,$t$;α} →→ N($k$) + ??{numsem},,,$t-1$;α{??{vsem},,$k$,;α} %4>%1 ??{numsem},,,$t-1$;α{??{ssem},,$k$,;α}
.endecl
	That is, in order for an {ssem} to occur, the
initial value of the semaphore plus the number of previous
{vsem} operations on the semaphore must exceed the number
of previous operations on the semaphore.  Thus, for example,
if the initial value is /0/, then no {ssem} operation
can occur (and thus no {psem} operation complete)
unless and until after a {vsem} operation occurs on the
semaphore.

.smallhead Rule B.  Bagging Semaphore Constraint

	The rules above describe the behavior of a system
using busy-wait semaphores.  This rule imposes an
additional constraint.

.beginecl
∀$t$ ∀$j$ ∀$k$ ??{vsem},$j$,$k$,$t$; ε α{??{osem},,,$t$;α} ∧ ??{numsem},,,$t-1$;α{??{rsem},,$k$,;α} %4>%* ??{numsem},,,$t-1$;α{??{ssem},,$k$,;α}
     →→ α{??{osem},,$k$,$t$($k$);α} = α{??{ssem},$j'$,$k$,$t$($k$);α}
.endecl
for some $j'$ such that
.beginecl
??{numsem},,,$t-1$;α{??{rsem},$j$,$k$,;α} %4>%* ??{numsem},,,$t-1$;α{??{ssem},$j$,$k$,;α}
.endecl
and indeed some such $j'$ must exist.
	That is, when a {vsem} occurs on a given semaphore
and some other process has previously performed an {rsem}
not matched by an {ssem}, then that other process is hanging
on the semaphore, and the next operation on the semaphore
must be to let some hanging process perform an {ssem}
and thereby proceed.
	This rule may seem at first sight not to be
sufficiently strong, since it does not take into account
%3N($k$)%1 or the number of {vsem}'s.  However, Rule 3
takes care of this; if there is an {rsem} operation
without a matching {ssem} pending when the {vsem} occurs,
then the {ssem} had been blocked from occurring.


.smallhead Rule Q.  Queuing Semaphore Constraint

	This is an alternative to Rule B.

.beginecl
∀$t$ ∀$j$ ∀$k$ ??{vsem},$j$,$k$,$t$; ε α{??{osem},,,$t$;α} ∧ ??{numsem},,,$t-1$;α{??{rsem},,$k$,;α} %4>%* ??{numsem},,,$t-1$;α{??{ssem},,$k$,;α}
     →→ α{??{osem},,$k$,$t$($k$);α} = α{??{ssem},$j'$,$k$,$t$($k$);α}
.endecl
for some $j'$ such that
.beginecl
??{numsem},,,$t-1$;α{??{rsem},$j$,$k$,;α} %4>%* ??{numsem},,,$t-1$;α{??{ssem},$j$,$k$,;α}
.endecl
and furthermore such that
.beginecl
{mu}$t'$[??{numsem},,,$t'$;α{??{rsem},$j$,$k$,;α} = ??{numsem},,,$t$;α{??{rsem},$j$,$k$,;α}]
.endecl
is minimized over the possible choices of $j'$.

	That is, when a {vsem} occurs on a given semaphore
and some other process has previously performed an {rsem}
not matched by an {ssem}, then that other process is hanging
on the semaphore, and the next operation on the semaphore
must be to let some hanging process perform an {ssem}
and thereby proceed.
Furthermore, if more than one process is hanging on the
semaphore, the one that is allowed to perform an {ssem}
must be the one which least recently performed the
mataching {rsem}, i.e. the one that has been waiting the
longest.
β